M:MsgA, l:IdLnk, mss:(M.Msg List). withlnk(l;mss)  ((tg:Id  M.dout(l,tg)) List) 

latex

Definitions	x:A. B(x), t  T, withlnk(l;mss), mapfilter(f;P;L), mlnk(m), t.1, P  Q, t.2, M.Msg, Msg(da), Msg(M), , P  Q, P & Q, M.dout(l,tg)
Lemmas	ma-msg wf, IdLnk wf, msga wf, filter type, eq lnk wf, assert wf, map wf, Id wf, ma-dout wf, assert-eq-lnk, subtype rel self